The behavior and operation of devices may be described using abstract state machines (ASMs). For each action that the device may take, the ASM defines conditions that must be met to effect changes to the state of the device. The conditions may be said to “guard” changes to the device state, and may thus be referred to as guards on the device state. In a normalized form, state settings for each action that the device may take are guarded by simple (e.g., non-nested) conditions. For a more complete description of normalized ASMs, see Yuri Gurevich, Evolving Algebra, 1993: Lipari Guide, in Egon Boerger, Specification and Validation Methods, pages 9-36, Oxford University Press, 1995 (hereafter “Evolving Algebra”). ASMs have applications beyond describing the behavior and operation of devices. For example, ASMs may describe the behavior and operation of software programs executing on a general purpose computer system.
Each unique combination of state settings represents a state of the device in the ASM. For this reason, ASMs may have a large, even infinite number of states. Languages exists for specifying model programs (i.e., AsmL®, Spec#, etc.). These languages often include interpreters that will reduce the specific model into a finite state machine.
Well known techniques exist for generating test suites from finite state machines (FSMs). FSMs define the behavior of a device in terms of device states and the events that result in state changes. However, due to the very large or infinite number of states of the ASMs, it is often impractical to apply to ASMs the techniques for generating test suites from FSMs. A previous patent application provides a manner of producing an FSM from an ASM (see “Generating a Test Suite from an Abstract State Machine,” U.S. patent application Ser. No. 10/071,524, filed Feb. 8, 2002, which is incorporated herein by reference and is hereafter referred to as “GTSASM”), which leads to the application of FSM test suite generation techniques to ASMs. This prior application provides a way of generating test suites from an ASM generated from a model program.
During test case generation from a model program, a finite transition system is produced that encodes interesting or relevant runs of the model program (a process called “FSM generation”), and then the finite transition system is traversed to produce test cases. The finite transition system produced from a model program can also be used to verify the behavior (e.g., inputs, outputs, etc.) of an implementation under test (e.g., device, software, etc.). Although a model program is expressed as a finite text, it typically induces a transition system (an “unwinding” of the model program) with a very large or even infinite state space.
FIG. 1 is a graphical representation of a test graph. As shown, the test graph provides three vertices 1, 2, and 3, and four edges a, b, c, d, and e. Behavioral coverage of this graph could be provided with a test suite comprising the following transition sequences,
[a]
[b, c]
[b, d, e].
Thus, a prior art method for generating test sequences, provides complete coverage of the test graph shown 100. However, other considerations arise in the context of non-deterministic testing or other reactive systems.